l:IdLnk, dt:tg:Id fp Type, tg:Id, T:Type. lnk-decl(l;dt)(rcv(l,tg))?T ~ dt(tg)?T 

latex

Definitions	x:A. B(x), t  T, x. t(x), f(x)?z, if b t else f fi, P  Q, true, false, Prop, rcv(l,tg), lnk-decl(l;dt), f(x), 2of(t), outl(x), x  dom(f), 1of(t), {T}, SQType(T), x:A. B(x), P & Q, x(s), , Unit, P  Q, A, False, a:A fp B(a), P  Q,
Lemmas	Id wf, fpf wf, IdLnk wf, fpf-dom wf, Knd wf, Kind-deq wf, lnk-decl wf, fpf-trivial-subtype-top, top wf, rcv wf, bool wf, eqtt to assert, id-deq wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, assert-deq-member, map wf, member map, rcv one one, Id sq, l member wf